val-axiom(E;V;M;info;pred?;
val-axiom(init;Trans;Choose;
val-axiom(Send;val)
== (e:E.
== (islocal(kind(e))
== ( isl(Choose(loc(e),act(kind(e)),state_when(e)))
== ( & val(e) = outl(Choose(loc(e),act(kind(e)),state_when(e))))
== & (e:E.
== & (isrcv(kind(e))
== & ( (<lnk(kind(e)),tag(kind(e)),(val(e))>  Send
== & ( (<lnk(kind(e)),tag(kind(e)),(val(e))>  (loc(sender(e))
== & ( (<lnk(kind(e)),tag(kind(e)),(val(e))>  ,kind(sender(e))
== & ( (<lnk(kind(e)),tag(kind(e)),(val(e))>  ,val(sender(e))
== & ( (<lnk(kind(e)),tag(kind(e)),(val(e))>  ,state_when(sender(e))))) 

latex

---

clarification:

val-axiom(E;V;M;info;pred?;
val-axiom(init;Trans;Choose;
val-axiom(Send;val)
== (e:E.
== (islocal(kind(info;e))
== ( isl(Choose(loc(info;e),act(kind(info;e)),state_when(e;info;pred?;init;Trans;val)))
== ( & val(e)
== ( & =
== ( & outl(Choose(loc(info;e),act(kind(info;e)),state_when(e;info;pred?;init;Trans;val)))
== ( &  V(loc(info;e),act(kind(info;e))))
== & (e:E.
== & (isrcv(kind(info;e))
== & ( (<lnk(kind(info;e))
== & ( (,tag(kind(info;e))
== & ( (,(val(e))>  Send
== & ( (,(val(e))>  (loc(info;sender(info;e))
== & ( (,(val(e))>  ,kind(info;sender(info;e))
== & ( (,(val(e))>  ,val(sender(info;e))
== & ( (,(val(e))>  ,state_when(sender(info;e);info;pred?;init;Trans;val))  Msg(M))) 

latex

Definitions	P & Q, islocal(k), A & B, isl(x), s = t, outl(x), act(k), x:A. B(x), P  Q, b, isrcv(k), (x  l), lnk(k), <a,b>, tag(k), loc(e), kind(e), f(a), state_when(e), sender(e), Msg(M)
FDL editor aliases	val-axiom